Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		x - 0	→ x
2:		s(x) - s(y)	→ x - y
3:		x * 0	→ 0
4:		x * s(y)	→ (x * y) + x
5:		if(true,x,y)	→ x
6:		if(false,x,y)	→ y
7:		odd(0)	→ false
8:		odd(s(0))	→ true
9:		odd(s(s(x)))	→ odd(x)
10:		half(0)	→ 0
11:		half(s(0))	→ 0
12:		half(s(s(x)))	→ s(half(x))
13:		if(true,x,y)	→ true
14:		if(false,x,y)	→ false
15:		pow(x,y)	→ f(x,y,s(0))
16:		f(x,0,z)	→ z
17:		f(x,s(y),z)	→ if(odd(s(y)),f(x,y,x * z),f(x * x,half(s(y)),z))

There are 12 dependency pairs:


18:		s(x) -# s(y)	→ x -# y
19:		x *# s(y)	→ x *# y
20:		ODD(s(s(x)))	→ ODD(x)
21:		HALF(s(s(x)))	→ HALF(x)
22:		POW(x,y)	→ F(x,y,s(0))
23:		F(x,s(y),z)	→ IF(odd(s(y)),f(x,y,x * z),f(x * x,half(s(y)),z))
24:		F(x,s(y),z)	→ ODD(s(y))
25:		F(x,s(y),z)	→ F(x,y,x * z)
26:		F(x,s(y),z)	→ x *# z
27:		F(x,s(y),z)	→ F(x * x,half(s(y)),z)
28:		F(x,s(y),z)	→ x *# x
29:		F(x,s(y),z)	→ HALF(s(y))

The approximated dependency graph contains 5 SCCs: {19}, {18}, {21}, {20} and {25,27}.

Consider the SCC {19}. There are no usable rules. By taking the AF π with π(*#) = 2 together with the lexicographic path order with empty precedence, rule 19 is strictly decreasing.

Consider the SCC {18}. There are no usable rules. By taking the AF π with π(-#) = 1 together with the lexicographic path order with empty precedence, rule 18 is strictly decreasing.

Consider the SCC {21}. There are no usable rules. By taking the AF π with π(HALF) = 1 together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.

Consider the SCC {20}. There are no usable rules. By taking the AF π with π(ODD) = 1 together with the lexicographic path order with empty precedence, rule 20 is strictly decreasing.

Consider the SCC {25,27}. The usable rules are {3,4,10-12}. By taking the AF π with π(+) = π(half) = 1 and π(*) = π(F) = 2 together with the lexicographic path order with empty precedence, the rules in {3,10,27} are weakly decreasing and the rules in {4,11,12,25} are strictly decreasing. There is one new SCC.
- Consider the SCC {27}. The constraints could not be solved.

Tyrolean Termination Tool (0.12 seconds) --- May 4, 2006